上一篇提到，Slither 的 detector 只能找已經寫成規則的問題。Level Finance 的重複領取漏洞就是一個沒有 Finding 的案例。

歷史事件與最小模型

Level Finance 是 BNB Chain 上的去中心化永續合約交易平台。2023 年 5 月，它的轉介紹獎勵合約 LevelReferralControllerV2 遭到攻擊。漏洞位在批次領取函式 claimMultiple，傳入的 epoch 陣列可以包含重複值，導致同一個 epoch 的獎勵被重複計算。

DeFiHackLabs 的 PoC 把根因記成「Lack of checking for duplicate elements in arrays」。PoC 的 claimReward(2000) 會建立長度 2000 的陣列，所有元素都放入同一個 epoch，再呼叫 claimMultiple。

真實合約的獎勵計算還包含 vesting 和已領金額，漏洞也跟 claimed 的更新方式有關。下面不是原合約的逐行還原，只保留「epoch 重複時，獎勵會被重複計算」的部分。

contract LevelRewardsVulnerable {
    mapping(uint256 epoch => uint256 reward) public rewardFor;
    mapping(address user => mapping(uint256 epoch => bool value)) public claimed;
    mapping(address user => uint256 amount) public paid;

    function setReward(uint256 epoch, uint256 reward) external {
        rewardFor[epoch] = reward;
    }

    function claimMultiple(uint256[] calldata epochs) external returns (uint256 payout) {
        for (uint256 i; i < epochs.length; ++i) {
            require(!claimed[msg.sender][epochs[i]], "already claimed");
            payout += rewardFor[epochs[i]];
        }

        for (uint256 i; i < epochs.length; ++i) {
            claimed[msg.sender][epochs[i]] = true;
        }

        paid[msg.sender] += payout;
    }
}

第一圈用 epochs[i] 當 key 檢查與累積，第二圈才標記。同一個 epoch 在陣列裡出現兩次時，兩次檢查都會通過。

Slither 的輸出

以下結果來自這份最小模型，不是鏈上原合約。Slither 只報了一筆 Informational：

Version constraint ^0.8.20 contains known severe issues
	- VerbatimInvalidDeduplication
	- FullInlinerNonExpressionSplitArgumentEvaluationOrder
	- MissingSideEffectsOnSelectorAccess.
It is used by:
	- ^0.8.20 (src/LevelCase.sol#2)

版本範圍 ^0.8.20 包含有已知問題的編譯器版本，所以 solc-version detector 發出警告。這筆 Finding 跟重複領取無關。

SlithIR

用下列指令可以看到 claimMultiple 的 SlithIR：

slither src/LevelCase.sol --print slithir

# 第一圈：檢查「還沒領過」
REF_2(mapping(uint256 => bool)) -> claimed[msg.sender]
REF_3(uint256) -> epochs[i]
REF_4(bool) -> REF_2[REF_3]
TMP_1 = UnaryType.BANG REF_4

# 第一圈：累積獎勵
REF_5(uint256) -> epochs[i]
REF_6(uint256) -> rewardFor[REF_5]
payout(uint256) = payout (c)+ REF_6

# 第二圈：標記已領
REF_8(mapping(uint256 => bool)) -> claimed[msg.sender]
REF_9(uint256) -> epochs[i_scope_0]
REF_10(bool) -> REF_8[REF_9]
REF_10(bool) (->claimed) := True(bool)

epochs[i] 同時當了 rewardFor 和 claimed 的 key。IR 裡有 mapping 的讀取，也有第二圈的 state update。Slither 已經保留 detector 需要的程式結構。

IR 不會自己判斷 epoch 能不能重複。這條限制要由 detector 或人工 review 補上。

Detector 沒有檢查 epoch 是否重複

Detector 各自檢查特定 pattern。Reentrancy detector 會找外部呼叫和 state update 的先後關係。這份最小模型需要比較同一次呼叫裡的陣列元素，確認不同位置有沒有相同的值。這次執行的 detectors 沒有做這項檢查。

可以把「使用者控制的陣列元素被拿來當 state key，而且檢查和更新分在不同迴圈」寫成自訂 detector。它只能指出需要確認的位置，不能直接證明重複領取一定成立。之後的篇章會實作這個 detector。

沒有 Finding 的檢查順序

看到「沒有 Finding」時，可以依序檢查：

1. 合約有沒有編譯成功，預期的 detectors 有沒有執行。
2. 相關的資料流和 state update 有沒有出現在 SlithIR。
3. 現有 detector 有沒有描述要檢查的規則。

這份最小模型有完成編譯和分析，相關操作也出現在 SlithIR。沒有 Finding 的原因是現有 detector 沒有檢查 epoch 是否重複。至於重複輸入能不能讓模型多付獎勵，要用可執行測試產生 counterexample，這部分留給 Foundry。

明日預告

明天會換成 reentrancy 案例，比較最小合約的 vulnerable / fixed 兩版和 Slither 的輸出。

參考資料

• DeFiHackLabs：Level Finance PoC
• Level Finance：Referral reward exploit remediation
• BscScan：攻擊交易
• Slither
• Solidity：已知編譯器問題